Contains definitions for integer functions such
as mod, floor, max and min.
Gives many standard lemmas for standard arithmetic
functions over the integers, involving both
equalities and inequalities.
At end, are some induction lemmas for
various subsets of the integers.
